1. Field
The invention disclosed and claimed herein generally pertains to a method for use with static analysis of a computer program, wherein the static analysis may show a very large number of discovered violations with respect to a given property. More particularly, the invention pertains to a method of the above type which can substantially reduce the number of discovered violations, by providing conditions for the correctness of the program with respect to the property.
2. Description of the Related Art
Static analysis of computer software enables sound checking to determine whether the subject program violates a property of interest. In security analysis, for example, the property may be vulnerable data flows from source statements (i.e. statements reading user-provided input), to sink statements (i.e. statements that perform security sensitive operations). Soundness in this context means that the analysis reports a superset of all the real, true or actual violations. As an example of security analysis, a security scanner is used which is guaranteed to report all vulnerable flows. However, the scanner may also report as vulnerable a number of flows which in fact are not vulnerable, due to the undecidability of static analysis. Such analysis has to conservatively compensate for (1) missing specifications and (2) genuinely dynamic behaviors, such as reflective code constructs.
In practice, this one-sided error typically yields a poor user interface. This is because a report produced by static analysis is often prohibitive in size, and can comprise thousands, or even tens of thousands, of findings for small-scale and medium scale applications. A static analysis report may also provide many more findings for industry-scale code. It is then up to the user to review all the reported findings, and decide which of them are true and which are spurious. From a usability standpoint, this interface, wherein all potential violations of the relevant property are output to the user, is responsible for many instances where correct problems plagued by the analysis tool are not addressed by the developer. There are often simply too many issues to consider, for the developer to be able to look into all of them.
The problem of overwhelming the user with a prohibitive number of security findings has been frequently acknowledged. The presently used solution is to fuse or merge together distinct findings that are similar or equivalent in some sense. In security analysis, the merge criterion can be based, for example, on the type of vulnerability, e.g., cross-site scripting, SQL injection, and the like, and on the source and sink statements. However, presently used merging is highly limited. Valuable information can be lost because issues are merged too aggressively. Also, the report of violations typically remains too large for practical use, and can still comprise hundreds if not thousands of issues.